The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

group3(@l) → group3#1(@l)
group3#1(::(@x, @xs)) → group3#2(@xs, @x)
group3#1(nil) → nil
group3#2(::(@y, @ys), @x) → group3#3(@ys, @x, @y)
group3#2(nil, @x) → nil
group3#3(::(@z, @zs), @x, @y) → ::(tuple#3(@x, @y, @z), group3(@zs))
group3#3(nil, @x, @y) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@x, @xs), @l2, @l3) → zip3#2(@l2, @l3, @x, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@y, @ys), @l3, @x, @xs) → zip3#3(@l3, @x, @xs, @y, @ys)
zip3#2(nil, @l3, @x, @xs) → nil
zip3#3(::(@z, @zs), @x, @xs, @y, @ys) → ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
zip3#3(nil, @x, @xs, @y, @ys) → nil

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

group3(@l) → group3#1(@l) [1]
group3#1(::(@x, @xs)) → group3#2(@xs, @x) [1]
group3#1(nil) → nil [1]
group3#2(::(@y, @ys), @x) → group3#3(@ys, @x, @y) [1]
group3#2(nil, @x) → nil [1]
group3#3(::(@z, @zs), @x, @y) → ::(tuple#3(@x, @y, @z), group3(@zs)) [1]
group3#3(nil, @x, @y) → nil [1]
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3) [1]
zip3#1(::(@x, @xs), @l2, @l3) → zip3#2(@l2, @l3, @x, @xs) [1]
zip3#1(nil, @l2, @l3) → nil [1]
zip3#2(::(@y, @ys), @l3, @x, @xs) → zip3#3(@l3, @x, @xs, @y, @ys) [1]
zip3#2(nil, @l3, @x, @xs) → nil [1]
zip3#3(::(@z, @zs), @x, @xs, @y, @ys) → ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) [1]
zip3#3(nil, @x, @xs, @y, @ys) → nil [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

group3(@l) → group3#1(@l) [1]
group3#1(::(@x, @xs)) → group3#2(@xs, @x) [1]
group3#1(nil) → nil [1]
group3#2(::(@y, @ys), @x) → group3#3(@ys, @x, @y) [1]
group3#2(nil, @x) → nil [1]
group3#3(::(@z, @zs), @x, @y) → ::(tuple#3(@x, @y, @z), group3(@zs)) [1]
group3#3(nil, @x, @y) → nil [1]
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3) [1]
zip3#1(::(@x, @xs), @l2, @l3) → zip3#2(@l2, @l3, @x, @xs) [1]
zip3#1(nil, @l2, @l3) → nil [1]
zip3#2(::(@y, @ys), @l3, @x, @xs) → zip3#3(@l3, @x, @xs, @y, @ys) [1]
zip3#2(nil, @l3, @x, @xs) → nil [1]
zip3#3(::(@z, @zs), @x, @xs, @y, @ys) → ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) [1]
zip3#3(nil, @x, @xs, @y, @ys) → nil [1]

The TRS has the following type information:

group3 :: :::nil → :::nil group3#1 :: :::nil → :::nil :: :: tuple#3 → :::nil → :::nil group3#2 :: :::nil → tuple#3 → :::nil nil :: :::nil group3#3 :: :::nil → tuple#3 → tuple#3 → :::nil tuple#3 :: tuple#3 → tuple#3 → tuple#3 → tuple#3 zip3 :: :::nil → :::nil → :::nil → :::nil zip3#1 :: :::nil → :::nil → :::nil → :::nil zip3#2 :: :::nil → :::nil → tuple#3 → :::nil → :::nil zip3#3 :: :::nil → tuple#3 → :::nil → tuple#3 → :::nil → :::nil

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

group3
group3#1
group3#2
group3#3
zip3
zip3#1
zip3#2
zip3#3

(c) The following functions are completely defined:
none

Due to the following rules being added:
none

And the following fresh constants:

const

(6) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: group3(@l) → group3#1(@l) [1] group3#1(::(@x, @xs)) → group3#2(@xs, @x) [1] group3#1(nil) → nil [1] group3#2(::(@y, @ys), @x) → group3#3(@ys, @x, @y) [1] group3#2(nil, @x) → nil [1] group3#3(::(@z, @zs), @x, @y) → ::(tuple#3(@x, @y, @z), group3(@zs)) [1] group3#3(nil, @x, @y) → nil [1] zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3) [1] zip3#1(::(@x, @xs), @l2, @l3) → zip3#2(@l2, @l3, @x, @xs) [1] zip3#1(nil, @l2, @l3) → nil [1] zip3#2(::(@y, @ys), @l3, @x, @xs) → zip3#3(@l3, @x, @xs, @y, @ys) [1] zip3#2(nil, @l3, @x, @xs) → nil [1] zip3#3(::(@z, @zs), @x, @xs, @y, @ys) → ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) [1] zip3#3(nil, @x, @xs, @y, @ys) → nil [1] The TRS has the following type information: group3 :: :::nil → :::nil group3#1 :: :::nil → :::nil :: :: tuple#3 → :::nil → :::nil group3#2 :: :::nil → tuple#3 → :::nil nil :: :::nil group3#3 :: :::nil → tuple#3 → tuple#3 → :::nil tuple#3 :: tuple#3 → tuple#3 → tuple#3 → tuple#3 zip3 :: :::nil → :::nil → :::nil → :::nil zip3#1 :: :::nil → :::nil → :::nil → :::nil zip3#2 :: :::nil → :::nil → tuple#3 → :::nil → :::nil zip3#3 :: :::nil → tuple#3 → :::nil → tuple#3 → :::nil → :::nil const :: tuple#3 Rewrite Strategy: INNERMOST

(7) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: group3(@l) → group3#1(@l) [1] group3#1(::(@x, @xs)) → group3#2(@xs, @x) [1] group3#1(nil) → nil [1] group3#2(::(@y, @ys), @x) → group3#3(@ys, @x, @y) [1] group3#2(nil, @x) → nil [1] group3#3(::(@z, @zs), @x, @y) → ::(tuple#3(@x, @y, @z), group3(@zs)) [1] group3#3(nil, @x, @y) → nil [1] zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3) [1] zip3#1(::(@x, @xs), @l2, @l3) → zip3#2(@l2, @l3, @x, @xs) [1] zip3#1(nil, @l2, @l3) → nil [1] zip3#2(::(@y, @ys), @l3, @x, @xs) → zip3#3(@l3, @x, @xs, @y, @ys) [1] zip3#2(nil, @l3, @x, @xs) → nil [1] zip3#3(::(@z, @zs), @x, @xs, @y, @ys) → ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) [1] zip3#3(nil, @x, @xs, @y, @ys) → nil [1] The TRS has the following type information: group3 :: :::nil → :::nil group3#1 :: :::nil → :::nil :: :: tuple#3 → :::nil → :::nil group3#2 :: :::nil → tuple#3 → :::nil nil :: :::nil group3#3 :: :::nil → tuple#3 → tuple#3 → :::nil tuple#3 :: tuple#3 → tuple#3 → tuple#3 → tuple#3 zip3 :: :::nil → :::nil → :::nil → :::nil zip3#1 :: :::nil → :::nil → :::nil → :::nil zip3#2 :: :::nil → :::nil → tuple#3 → :::nil → :::nil zip3#3 :: :::nil → tuple#3 → :::nil → tuple#3 → :::nil → :::nil const :: tuple#3 Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

nil => 0
const => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

group3(z) -{ 1 }→ group3#1(@l) :|: z = @l, @l >= 0
group3#1(z) -{ 1 }→ group3#2(@xs, @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
group3#1(z) -{ 1 }→ 0 :|: z = 0
group3#2(z, z') -{ 1 }→ group3#3(@ys, @x, @y) :|: z = 1 + @y + @ys, @x >= 0, @y >= 0, z' = @x, @ys >= 0
group3#2(z, z') -{ 1 }→ 0 :|: @x >= 0, z = 0, z' = @x
group3#3(z, z', z'') -{ 1 }→ 0 :|: @x >= 0, z = 0, @y >= 0, z' = @x, z'' = @y
group3#3(z, z', z'') -{ 1 }→ 1 + (1 + @x + @y + @z) + group3(@zs) :|: @x >= 0, z = 1 + @z + @zs, @zs >= 0, @y >= 0, z' = @x, z'' = @y, @z >= 0
zip3(z, z', z'') -{ 1 }→ zip3#1(@l1, @l2, @l3) :|: @l1 >= 0, z' = @l2, @l2 >= 0, @l3 >= 0, z = @l1, z'' = @l3
zip3#1(z, z', z'') -{ 1 }→ zip3#2(@l2, @l3, @x, @xs) :|: z' = @l2, @x >= 0, z = 1 + @x + @xs, @l2 >= 0, @l3 >= 0, @xs >= 0, z'' = @l3
zip3#1(z, z', z'') -{ 1 }→ 0 :|: z' = @l2, @l2 >= 0, @l3 >= 0, z'' = @l3, z = 0
zip3#2(z, z', z'', z1) -{ 1 }→ zip3#3(@l3, @x, @xs, @y, @ys) :|: z = 1 + @y + @ys, @x >= 0, @l3 >= 0, z1 = @xs, @xs >= 0, z'' = @x, @y >= 0, z' = @l3, @ys >= 0
zip3#2(z, z', z'', z1) -{ 1 }→ 0 :|: @x >= 0, @l3 >= 0, z1 = @xs, @xs >= 0, z = 0, z'' = @x, z' = @l3
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 0 :|: @x >= 0, z1 = @y, @xs >= 0, z2 = @ys, z = 0, @y >= 0, z' = @x, z'' = @xs, @ys >= 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 1 + (1 + @x + @y + @z) + zip3(@xs, @ys, @zs) :|: @x >= 0, z1 = @y, @xs >= 0, z2 = @ys, z = 1 + @z + @zs, @zs >= 0, @y >= 0, z' = @x, z'' = @xs, @ys >= 0, @z >= 0

(11) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(12) Obligation:

Complexity RNTS consisting of the following rules:

group3(z) -{ 1 }→ group3#1(z) :|: z >= 0
group3#1(z) -{ 1 }→ group3#2(@xs, @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
group3#1(z) -{ 1 }→ 0 :|: z = 0
group3#2(z, z') -{ 1 }→ group3#3(@ys, z', @y) :|: z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
group3#2(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
group3#3(z, z', z'') -{ 1 }→ 0 :|: z' >= 0, z = 0, z'' >= 0
group3#3(z, z', z'') -{ 1 }→ 1 + (1 + z' + z'' + @z) + group3(@zs) :|: z' >= 0, z = 1 + @z + @zs, @zs >= 0, z'' >= 0, @z >= 0
zip3(z, z', z'') -{ 1 }→ zip3#1(z, z', z'') :|: z >= 0, z' >= 0, z'' >= 0
zip3#1(z, z', z'') -{ 1 }→ zip3#2(z', z'', @x, @xs) :|: @x >= 0, z = 1 + @x + @xs, z' >= 0, z'' >= 0, @xs >= 0
zip3#1(z, z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' >= 0, z = 0
zip3#2(z, z', z'', z1) -{ 1 }→ zip3#3(z', z'', z1, @y, @ys) :|: z = 1 + @y + @ys, z'' >= 0, z' >= 0, z1 >= 0, @y >= 0, @ys >= 0
zip3#2(z, z', z'', z1) -{ 1 }→ 0 :|: z'' >= 0, z' >= 0, z1 >= 0, z = 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 0 :|: z' >= 0, z'' >= 0, z = 0, z1 >= 0, z2 >= 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 1 + (1 + z' + z1 + @z) + zip3(z'', z2, @zs) :|: z' >= 0, z'' >= 0, z = 1 + @z + @zs, @zs >= 0, z1 >= 0, z2 >= 0, @z >= 0

(13) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ group3#2, group3#1, group3, group3#3 } { zip3#3, zip3#2, zip3#1, zip3 }

(14) Obligation:

Complexity RNTS consisting of the following rules:

group3(z) -{ 1 }→ group3#1(z) :|: z >= 0
group3#1(z) -{ 1 }→ group3#2(@xs, @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
group3#1(z) -{ 1 }→ 0 :|: z = 0
group3#2(z, z') -{ 1 }→ group3#3(@ys, z', @y) :|: z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
group3#2(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
group3#3(z, z', z'') -{ 1 }→ 0 :|: z' >= 0, z = 0, z'' >= 0
group3#3(z, z', z'') -{ 1 }→ 1 + (1 + z' + z'' + @z) + group3(@zs) :|: z' >= 0, z = 1 + @z + @zs, @zs >= 0, z'' >= 0, @z >= 0
zip3(z, z', z'') -{ 1 }→ zip3#1(z, z', z'') :|: z >= 0, z' >= 0, z'' >= 0
zip3#1(z, z', z'') -{ 1 }→ zip3#2(z', z'', @x, @xs) :|: @x >= 0, z = 1 + @x + @xs, z' >= 0, z'' >= 0, @xs >= 0
zip3#1(z, z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' >= 0, z = 0
zip3#2(z, z', z'', z1) -{ 1 }→ zip3#3(z', z'', z1, @y, @ys) :|: z = 1 + @y + @ys, z'' >= 0, z' >= 0, z1 >= 0, @y >= 0, @ys >= 0
zip3#2(z, z', z'', z1) -{ 1 }→ 0 :|: z'' >= 0, z' >= 0, z1 >= 0, z = 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 0 :|: z' >= 0, z'' >= 0, z = 0, z1 >= 0, z2 >= 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 1 + (1 + z' + z1 + @z) + zip3(z'', z2, @zs) :|: z' >= 0, z'' >= 0, z = 1 + @z + @zs, @zs >= 0, z1 >= 0, z2 >= 0, @z >= 0

Function symbols to be analyzed: {group3#2,group3#1,group3,group3#3}, {zip3#3,zip3#2,zip3#1,zip3}

(15) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: group3#2
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z + z'

Computed SIZE bound using CoFloCo for: group3#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

Computed SIZE bound using CoFloCo for: group3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

Computed SIZE bound using CoFloCo for: group3#3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z + z' + z''

(16) Obligation:

Complexity RNTS consisting of the following rules:

group3(z) -{ 1 }→ group3#1(z) :|: z >= 0
group3#1(z) -{ 1 }→ group3#2(@xs, @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
group3#1(z) -{ 1 }→ 0 :|: z = 0
group3#2(z, z') -{ 1 }→ group3#3(@ys, z', @y) :|: z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
group3#2(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
group3#3(z, z', z'') -{ 1 }→ 0 :|: z' >= 0, z = 0, z'' >= 0
group3#3(z, z', z'') -{ 1 }→ 1 + (1 + z' + z'' + @z) + group3(@zs) :|: z' >= 0, z = 1 + @z + @zs, @zs >= 0, z'' >= 0, @z >= 0
zip3(z, z', z'') -{ 1 }→ zip3#1(z, z', z'') :|: z >= 0, z' >= 0, z'' >= 0
zip3#1(z, z', z'') -{ 1 }→ zip3#2(z', z'', @x, @xs) :|: @x >= 0, z = 1 + @x + @xs, z' >= 0, z'' >= 0, @xs >= 0
zip3#1(z, z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' >= 0, z = 0
zip3#2(z, z', z'', z1) -{ 1 }→ zip3#3(z', z'', z1, @y, @ys) :|: z = 1 + @y + @ys, z'' >= 0, z' >= 0, z1 >= 0, @y >= 0, @ys >= 0
zip3#2(z, z', z'', z1) -{ 1 }→ 0 :|: z'' >= 0, z' >= 0, z1 >= 0, z = 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 0 :|: z' >= 0, z'' >= 0, z = 0, z1 >= 0, z2 >= 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 1 + (1 + z' + z1 + @z) + zip3(z'', z2, @zs) :|: z' >= 0, z'' >= 0, z = 1 + @z + @zs, @zs >= 0, z1 >= 0, z2 >= 0, @z >= 0

Function symbols to be analyzed: {group3#2,group3#1,group3,group3#3}, {zip3#3,zip3#2,zip3#1,zip3}
Previous analysis results are:

group3#2: runtime: ?, size: O(n1) [1 + z + z'] group3#1: runtime: ?, size: O(n1) [z] group3: runtime: ?, size: O(n1) [z] group3#3: runtime: ?, size: O(n1) [1 + z + z' + z'']

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using PUBS for: group3#2
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 4 + 4·z

Computed RUNTIME bound using CoFloCo for: group3#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 4·z

Computed RUNTIME bound using CoFloCo for: group3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + 4·z

Computed RUNTIME bound using CoFloCo for: group3#3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 4·z

(18) Obligation:

Complexity RNTS consisting of the following rules:

group3(z) -{ 1 }→ group3#1(z) :|: z >= 0
group3#1(z) -{ 1 }→ group3#2(@xs, @x) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0
group3#1(z) -{ 1 }→ 0 :|: z = 0
group3#2(z, z') -{ 1 }→ group3#3(@ys, z', @y) :|: z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
group3#2(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
group3#3(z, z', z'') -{ 1 }→ 0 :|: z' >= 0, z = 0, z'' >= 0
group3#3(z, z', z'') -{ 1 }→ 1 + (1 + z' + z'' + @z) + group3(@zs) :|: z' >= 0, z = 1 + @z + @zs, @zs >= 0, z'' >= 0, @z >= 0
zip3(z, z', z'') -{ 1 }→ zip3#1(z, z', z'') :|: z >= 0, z' >= 0, z'' >= 0
zip3#1(z, z', z'') -{ 1 }→ zip3#2(z', z'', @x, @xs) :|: @x >= 0, z = 1 + @x + @xs, z' >= 0, z'' >= 0, @xs >= 0
zip3#1(z, z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' >= 0, z = 0
zip3#2(z, z', z'', z1) -{ 1 }→ zip3#3(z', z'', z1, @y, @ys) :|: z = 1 + @y + @ys, z'' >= 0, z' >= 0, z1 >= 0, @y >= 0, @ys >= 0
zip3#2(z, z', z'', z1) -{ 1 }→ 0 :|: z'' >= 0, z' >= 0, z1 >= 0, z = 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 0 :|: z' >= 0, z'' >= 0, z = 0, z1 >= 0, z2 >= 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 1 + (1 + z' + z1 + @z) + zip3(z'', z2, @zs) :|: z' >= 0, z'' >= 0, z = 1 + @z + @zs, @zs >= 0, z1 >= 0, z2 >= 0, @z >= 0

Function symbols to be analyzed: {zip3#3,zip3#2,zip3#1,zip3}
Previous analysis results are:

group3#2: runtime: O(n1) [4 + 4·z], size: O(n1) [1 + z + z'] group3#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] group3: runtime: O(n1) [2 + 4·z], size: O(n1) [z] group3#3: runtime: O(n1) [1 + 4·z], size: O(n1) [1 + z + z' + z'']

(19) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(20) Obligation:

Complexity RNTS consisting of the following rules:

group3(z) -{ 2 + 4·z }→ s :|: s >= 0, s <= 1 * z, z >= 0
group3#1(z) -{ 5 + 4·@xs }→ s' :|: s' >= 0, s' <= 1 * @xs + 1 * @x + 1, @x >= 0, z = 1 + @x + @xs, @xs >= 0
group3#1(z) -{ 1 }→ 0 :|: z = 0
group3#2(z, z') -{ 2 + 4·@ys }→ s'' :|: s'' >= 0, s'' <= 1 * @ys + 1 * z' + 1 * @y + 1, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
group3#2(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
group3#3(z, z', z'') -{ 1 }→ 0 :|: z' >= 0, z = 0, z'' >= 0
group3#3(z, z', z'') -{ 3 + 4·@zs }→ 1 + (1 + z' + z'' + @z) + s1 :|: s1 >= 0, s1 <= 1 * @zs, z' >= 0, z = 1 + @z + @zs, @zs >= 0, z'' >= 0, @z >= 0
zip3(z, z', z'') -{ 1 }→ zip3#1(z, z', z'') :|: z >= 0, z' >= 0, z'' >= 0
zip3#1(z, z', z'') -{ 1 }→ zip3#2(z', z'', @x, @xs) :|: @x >= 0, z = 1 + @x + @xs, z' >= 0, z'' >= 0, @xs >= 0
zip3#1(z, z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' >= 0, z = 0
zip3#2(z, z', z'', z1) -{ 1 }→ zip3#3(z', z'', z1, @y, @ys) :|: z = 1 + @y + @ys, z'' >= 0, z' >= 0, z1 >= 0, @y >= 0, @ys >= 0
zip3#2(z, z', z'', z1) -{ 1 }→ 0 :|: z'' >= 0, z' >= 0, z1 >= 0, z = 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 0 :|: z' >= 0, z'' >= 0, z = 0, z1 >= 0, z2 >= 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 1 + (1 + z' + z1 + @z) + zip3(z'', z2, @zs) :|: z' >= 0, z'' >= 0, z = 1 + @z + @zs, @zs >= 0, z1 >= 0, z2 >= 0, @z >= 0

Function symbols to be analyzed: {zip3#3,zip3#2,zip3#1,zip3}
Previous analysis results are:

group3#2: runtime: O(n1) [4 + 4·z], size: O(n1) [1 + z + z'] group3#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] group3: runtime: O(n1) [2 + 4·z], size: O(n1) [z] group3#3: runtime: O(n1) [1 + 4·z], size: O(n1) [1 + z + z' + z'']

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: zip3#3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z + z' + z'' + z1 + z2

Computed SIZE bound using CoFloCo for: zip3#2
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z' + z'' + z1

Computed SIZE bound using KoAT for: zip3#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z' + z''

Computed SIZE bound using CoFloCo for: zip3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z' + z''

(22) Obligation:

Complexity RNTS consisting of the following rules:

group3(z) -{ 2 + 4·z }→ s :|: s >= 0, s <= 1 * z, z >= 0
group3#1(z) -{ 5 + 4·@xs }→ s' :|: s' >= 0, s' <= 1 * @xs + 1 * @x + 1, @x >= 0, z = 1 + @x + @xs, @xs >= 0
group3#1(z) -{ 1 }→ 0 :|: z = 0
group3#2(z, z') -{ 2 + 4·@ys }→ s'' :|: s'' >= 0, s'' <= 1 * @ys + 1 * z' + 1 * @y + 1, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
group3#2(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
group3#3(z, z', z'') -{ 1 }→ 0 :|: z' >= 0, z = 0, z'' >= 0
group3#3(z, z', z'') -{ 3 + 4·@zs }→ 1 + (1 + z' + z'' + @z) + s1 :|: s1 >= 0, s1 <= 1 * @zs, z' >= 0, z = 1 + @z + @zs, @zs >= 0, z'' >= 0, @z >= 0
zip3(z, z', z'') -{ 1 }→ zip3#1(z, z', z'') :|: z >= 0, z' >= 0, z'' >= 0
zip3#1(z, z', z'') -{ 1 }→ zip3#2(z', z'', @x, @xs) :|: @x >= 0, z = 1 + @x + @xs, z' >= 0, z'' >= 0, @xs >= 0
zip3#1(z, z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' >= 0, z = 0
zip3#2(z, z', z'', z1) -{ 1 }→ zip3#3(z', z'', z1, @y, @ys) :|: z = 1 + @y + @ys, z'' >= 0, z' >= 0, z1 >= 0, @y >= 0, @ys >= 0
zip3#2(z, z', z'', z1) -{ 1 }→ 0 :|: z'' >= 0, z' >= 0, z1 >= 0, z = 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 0 :|: z' >= 0, z'' >= 0, z = 0, z1 >= 0, z2 >= 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 1 + (1 + z' + z1 + @z) + zip3(z'', z2, @zs) :|: z' >= 0, z'' >= 0, z = 1 + @z + @zs, @zs >= 0, z1 >= 0, z2 >= 0, @z >= 0

Function symbols to be analyzed: {zip3#3,zip3#2,zip3#1,zip3}
Previous analysis results are:

group3#2: runtime: O(n1) [4 + 4·z], size: O(n1) [1 + z + z'] group3#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] group3: runtime: O(n1) [2 + 4·z], size: O(n1) [z] group3#3: runtime: O(n1) [1 + 4·z], size: O(n1) [1 + z + z' + z''] zip3#3: runtime: ?, size: O(n1) [1 + z + z' + z'' + z1 + z2] zip3#2: runtime: ?, size: O(n1) [z + z' + z'' + z1] zip3#1: runtime: ?, size: O(n1) [z + z' + z''] zip3: runtime: ?, size: O(n1) [z + z' + z'']

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: zip3#3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 4 + 4·z2

Computed RUNTIME bound using CoFloCo for: zip3#2
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 4·z

Computed RUNTIME bound using CoFloCo for: zip3#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + 4·z'

Computed RUNTIME bound using CoFloCo for: zip3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 3 + 4·z'

(24) Obligation:

Complexity RNTS consisting of the following rules:

group3(z) -{ 2 + 4·z }→ s :|: s >= 0, s <= 1 * z, z >= 0
group3#1(z) -{ 5 + 4·@xs }→ s' :|: s' >= 0, s' <= 1 * @xs + 1 * @x + 1, @x >= 0, z = 1 + @x + @xs, @xs >= 0
group3#1(z) -{ 1 }→ 0 :|: z = 0
group3#2(z, z') -{ 2 + 4·@ys }→ s'' :|: s'' >= 0, s'' <= 1 * @ys + 1 * z' + 1 * @y + 1, z = 1 + @y + @ys, z' >= 0, @y >= 0, @ys >= 0
group3#2(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
group3#3(z, z', z'') -{ 1 }→ 0 :|: z' >= 0, z = 0, z'' >= 0
group3#3(z, z', z'') -{ 3 + 4·@zs }→ 1 + (1 + z' + z'' + @z) + s1 :|: s1 >= 0, s1 <= 1 * @zs, z' >= 0, z = 1 + @z + @zs, @zs >= 0, z'' >= 0, @z >= 0
zip3(z, z', z'') -{ 1 }→ zip3#1(z, z', z'') :|: z >= 0, z' >= 0, z'' >= 0
zip3#1(z, z', z'') -{ 1 }→ zip3#2(z', z'', @x, @xs) :|: @x >= 0, z = 1 + @x + @xs, z' >= 0, z'' >= 0, @xs >= 0
zip3#1(z, z', z'') -{ 1 }→ 0 :|: z' >= 0, z'' >= 0, z = 0
zip3#2(z, z', z'', z1) -{ 1 }→ zip3#3(z', z'', z1, @y, @ys) :|: z = 1 + @y + @ys, z'' >= 0, z' >= 0, z1 >= 0, @y >= 0, @ys >= 0
zip3#2(z, z', z'', z1) -{ 1 }→ 0 :|: z'' >= 0, z' >= 0, z1 >= 0, z = 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 0 :|: z' >= 0, z'' >= 0, z = 0, z1 >= 0, z2 >= 0
zip3#3(z, z', z'', z1, z2) -{ 1 }→ 1 + (1 + z' + z1 + @z) + zip3(z'', z2, @zs) :|: z' >= 0, z'' >= 0, z = 1 + @z + @zs, @zs >= 0, z1 >= 0, z2 >= 0, @z >= 0

Function symbols to be analyzed:
Previous analysis results are:

group3#2: runtime: O(n1) [4 + 4·z], size: O(n1) [1 + z + z'] group3#1: runtime: O(n1) [1 + 4·z], size: O(n1) [z] group3: runtime: O(n1) [2 + 4·z], size: O(n1) [z] group3#3: runtime: O(n1) [1 + 4·z], size: O(n1) [1 + z + z' + z''] zip3#3: runtime: O(n1) [4 + 4·z2], size: O(n1) [1 + z + z' + z'' + z1 + z2] zip3#2: runtime: O(n1) [1 + 4·z], size: O(n1) [z + z' + z'' + z1] zip3#1: runtime: O(n1) [2 + 4·z'], size: O(n1) [z + z' + z''] zip3: runtime: O(n1) [3 + 4·z'], size: O(n1) [z + z' + z'']

(25) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(26) BOUNDS(1, n^1)